T:Type, A:(T). (x:T. Dec(A(x)))  ((x:T. Stable{A(x)}) & (f:detach_fun(T;A). True)) 

latex

Up	gen algebra 1
Definitions	t  T, P  Q, P  Q, x:A. B(x), P & Q, P  Q, , x:A. B(x), x. t(x), x(s), {T}
Lemmas	true wf, detach fun wf, stable wf, decidable wf, stable from decidable, exists det fun, sq stable from decidable, squash elim, decidable functionality, squash wf, all functionality wrt iff, exists det fun a, sq stable from stable